i:Id, A, B:MsgA. interface-compatible((@i A);(@i B)) 

latex

Definitions	(@i M), interface-compatible(A;B), interface-link(A;B;l;tg), M.dout(l,tg), , M.din(l,tg), rcv(l,tg) declared in M, mk-ma, MsgA, Valtype(da;k), Id, IdLnk, source(l), Unit, P  Q, a = b, destination(l), , b, KindDeq, b, x  dom(f), rcv(l,tg), a:A fp B(a), Knd, x. t(x), P  Q, Prop, t  T, A, x:A. B(x), P & Q, False
Lemmas	not wf, false wf, fpf-trivial-subtype-top, fpf-dom wf, assert wf, Knd wf, rcv wf, Kind-deq wf, bnot wf, ldst wf, eq id wf, assert of bnot, eqff to assert, iff transitivity, eqtt to assert, bool wf, lsrc wf, IdLnk wf, Id wf, msga wf